Nuprl Lemma : void-list-equality3
0,22
postcript
pdf
x
,
y
:Void List.
x
=
y
{null(
x
) & null(
y
)}
latex
Definitions
t
T
,
True
,
P
&
Q
,
{
T
}
,
Void
,
type
List
,
nil
,
s
=
t
,
Prop
,
x
:
A
B
(
x
)
,
P
Q
,
b
,
x
:
A
B
(
x
)
,
x
:
A
.
B
(
x
)
origin
x, y:Void List. x = y 
{null(x) & null(y)} x, y:Void List. x = y {null(x) & null(y)} 
T
B(x) Q
b
B(x)x:A. B(x)